\begin{tabbing}
$\forall$${\it es}$:event\_system\{i:l\}. 
\\[0ex]es{-}Trans(${\it es}$)
\\[0ex]$\in$ \=$i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.(es{-}V(${\it es}$)($i$,$a$)); $l$,$t$.(es{-}M(${\it es}$)($l$,$t$)))$\rightarrow$es\_state(${\it es}$; $i$)$\rightarrow$\+
\\[0ex]es\_state(${\it es}$; $i$)
\-
\end{tabbing}